ACL2 es un demostrador automatizado de teoremas con una lógica basada en un subconjunto aplicativo del lenguaje
Common Lisp. También está escrito es ese mismo sublenguaje y puede correr en diversas implementaciones de Common Lisp. Tiene un alto grado de automatismo y los programas escritos en
ACL2 pueden ser ejecutados en Common Lisp directamente.
ACL2 es la versión industrial del demostrador NQTHM de Boyer-Moore.